FDL - Nuprl Lemma : all_quot_elim

Nuprl Lemma : all_quot_elim

T:Type, E:(T

T

).
EquivRel(T;x,y.E(x,y))

(

F:((x,y:T//E(x,y))

).

(

w:(x,y:T//E(x,y)). SqStable(F(w)))

((

z:(x,y:T//E(x,y)). F(z))

(

z:T. F(z))))

Up quot 1, quot 1

Definitions x(s), x(s1,s2), x,y. t(x;y), t T, P Q, P & Q, P Q, P Q, , x:A. B(x), True, T, SqStable(P), S T

Lemmas equiv rel wf, sq stable wf, quotient qinc, quotient wf, squash wf